using System;
using ExternalLib;
using ExternalLib2;
using FieldAccessExtractor;
using Microsoft.Pex.Framework;
using Covana.ProblemExtractor;

namespace Benchmarks
{
    [PexClass]
    [InsufficientObjectFactoryObserver]
    [FieldAccessObserver]
//    [ResultTracingObserver]
    [BoundaryProblemObserver]
    public partial class ToyTest
    {
        [PexMethod]
        public void TestMETHOD(int i)
        {
            if (i > 5)
            {
                Console.WriteLine("1");
            }
            else
            {
                Console.WriteLine("2");
            }

            for (int j = 0; j < i; j++)
            {
                Console.WriteLine("3");
            }
        }

        [PexMethod]
        public void TestMETHOD2(int i)
        {
            switch (i)
            {
                case 1:
                    Console.WriteLine("1");
                    break;
                case 2:
                    Console.WriteLine("1");
                    break;
                case 3:
                    throw new Exception("exception");
                    break;
                case 4:
                    for (int j = 0; j < i; j++)
                    {
                        Console.WriteLine("cool");
                    }
                    break;
            }
        }


        [PexMethod]
        public void TestChildPlayToy([PexAssumeNotNull] Toy obj)
        {
            Child child = new Child(10);
            child.MakeChange(obj);
            if (obj.PlayedTimes > 5)
            {
                Console.WriteLine("yes");
            }
            else
            {
                Console.WriteLine("no");
            }
        }

        [PexMethod]
        public void TestChildDoNothing(Toy obj)
        {
            Child child = new Child(10);
            child.DoNothing(obj);
            if (obj.PlayedTimes > 5)
            {
                Console.WriteLine("yes");
            }
            else
            {
                Console.WriteLine("no");
            }
        }

        [PexMethod]
        public void TestToy(Toy toy)
        {
            if (toy.PlayedTimes > 5)
            {
                Console.WriteLine("yes");
            }
            else
            {
                Console.WriteLine("no");
            }
        }
    }
}